package engine;

import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;

import org.apache.log4j.Logger;
import org.apache.log4j.PropertyConfigurator;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.ModelIterator;

import cnf.Hints;
import cnf.Rules;
import data.Board;
import data.Constant;
import file.FormGenerator;
import file.HintParser;

public class Main {

	private static final Logger logger = Logger.getLogger(Main.class);

	public static void main(String args[]) {

		PropertyConfigurator.configure(ClassLoader
				.getSystemResource(Constant.LOG_CONFIG_FILE));

		final int MAXVAR = 40000;
		final int NBCLAUSES = 100000;

		FileWriter fstream = null;
		try {
			fstream = new FileWriter("summary.txt");
			
		} catch (IOException e1) {
			// TODO Auto-generated catch block
			e1.printStackTrace();
		}
		BufferedWriter summary_out = new BufferedWriter(fstream);
		
		ISolver solver;
		Rules rules;
		Hints hints;
		int[] model;
		boolean state = false;
		FormGenerator fg;
		HintParser hp;
		int solutions = 0;
		long start;
		int numUnsolvableBoards = 0;

		if (args == null) {
			logger.error("Wrong argument");
		} else {
			if (args.length != 1) {
				logger.error("Wrong argument");
			} else {
				hp = new HintParser(new File(args[0]));

				solver = new ModelIterator(SolverFactory.newDefault(), 100);
				// prepare the solver to accept MAXVAR variables.
				// MANDATORY
				solver.newVar(MAXVAR);
				// not mandatory for SAT solving. MANDATORY for
				// MAXSAT solving
				solver.setExpectedNumberOfClauses(NBCLAUSES);
				solver.setTimeout(3600); // 1 hour timeout

				try {
					if (hp.getBoards() != null) {
						for (Board board : hp.getBoards()) {
							state = false;
							long free = Runtime.getRuntime().freeMemory();

							start = System.currentTimeMillis();

							fg = new FormGenerator(MAXVAR, NBCLAUSES);
							rules = new Rules(solver, fg);
							logger.debug("Add rules");
							rules.setup();
							hints = new Hints(solver, fg);

							if (board.getColumnHint() != null) {
								logger.debug("Add column hints");
								hints.addColumnHint(board.getColumnHint());
							}
							if (board.getRowHint() != null) {
								logger.debug("Add row hints");
								hints.addRowHint(board.getRowHint());
							}
							if (board.getTileHints() != null) {
								logger.debug("Add tile hints");
								for (String tH : board.getTileHints()) {
									hints.addTileHint(tH);
								}
							}
							Hints.sS = 1001;
							fg.finish();
							logger.debug("Memory changes: "
									+ (Runtime.getRuntime().freeMemory() - free));
							free = Runtime.getRuntime().freeMemory();

							logger.info("Use "
									+ (System.currentTimeMillis() - start)
									+ "ms to generate rules for board "
									+ board.getBoardId());
							start = System.currentTimeMillis();

							// we are done. Working now on the IProblem
							// interface
							int c;
							int v;
							while (solver.isSatisfiable()) {
								solutions++;
								state = true;
								model = solver.model();
								String bufDia = "";

								// Draw upper border
								for (int i = -1; i <= Rules.CMAX + 1; i++) {
									if (i > Rules.CMAX) {
										bufDia += "#";
									} else {
										bufDia += "# ";
									}
								}
								bufDia += Constant.LINE_BREAK;

								// Draw content
								for (int i : model) {
									if (i > 0 && i < 1000) {
										c = (i % 100) / 10;
										v = (i % 10);

										if (v != 0 && v <= 7) {
											if (c == Rules.CMIN) {
												bufDia += "# ";
											} else {
												bufDia += " ";
											}

											switch (v) {
											case Constant.CIRCLE:
												bufDia += "c";
												break;
											case Constant.MIDDLE:
												bufDia += "m";
												break;
											case Constant.TOP:
												bufDia += "t";
												break;
											case Constant.BOTTOM:
												bufDia += "b";
												break;
											case Constant.LEFT:
												bufDia += "l";
												break;
											case Constant.RIGHT:
												bufDia += "r";
												break;
											case Constant.WATER:
												bufDia += "-";
												break;
											default:
												break;
											}

											if (c == Rules.CMAX) {
												bufDia += " #"
														+ Constant.LINE_BREAK;
											}
										}

									}
								}
								// Draw bottom border
								for (int i = -1; i <= Rules.CMAX + 1; i++) {
									if (i > Rules.CMAX) {
										bufDia += "#";
									} else {
										bufDia += "# ";
									}
								}
								logger.info("Find a solution for board "
										+ board.getBoardId()
										+ ", time consumed "
										+ (System.currentTimeMillis() - start)
										+ "ms: " + Constant.LINE_BREAK + bufDia);
								try {
									summary_out.write(board.getBoardId()+" "+solver.nVars()+" "+solver.nConstraints()+" "+
											(System.currentTimeMillis() - start)+Constant.LINE_BREAK);
								} catch (IOException e) {
									// TODO Auto-generated catch block
									e.printStackTrace();
								}

							}
							if (!state) {
								logger.info("No solution is found for board "
										+ board.getBoardId());
								numUnsolvableBoards++;
								try {
									summary_out.write(board.getBoardId()+" "+solver.nVars()+" "+solver.nConstraints()+" "+
											"-1"+Constant.LINE_BREAK);
								} catch (IOException e) {
									// TODO Auto-generated catch block
									e.printStackTrace();
								}
							} else {
								logger.info(Integer.toString(solutions)
										+ " solution(s) found for board "
										+ board.getBoardId());
								solutions = 0;
							}
							logger.debug("Memory changes: "
									+ (Runtime.getRuntime().freeMemory() - free));
							free = Runtime.getRuntime().freeMemory();
							solver.reset();
						}
					}

					logger.info("Total Boards: "+hp.getBoards().length);
					logger.info("Unsolvable Boards: "+numUnsolvableBoards);
					
					try {
						summary_out.close();
					} catch (IOException e) {
						// TODO Auto-generated catch block
						e.printStackTrace();
					}
				} catch (TimeoutException e) {
					logger.error("Problem takes too long time to solve");
				}
			}
		}
	}
}
